Section: New Results

Session Types

Session types describe communication protocols between two or more participants by specifying the sequence of exchanged messages, together with their functionality (sender, receiver and type of carried data). They may be viewed as the analogue, for concurrency and distribution, of data types for sequential computation. Originally conceived as a static analysis technique for an enhanced version of the $\pi$-calculus, session types have now been embedded into a range of functional, concurrent, and object-oriented programming languages.

We have pursued our work on session types along three main directions.

Multiparty Reactive Sessions

Ensuring that communication-centric systems interact according to an intended protocol is an important but difficult problem, particularly for systems with some reactive or timed components. To rise to this challenge, we have studied the integration of session-based concurrency and Synchronous Reactive Programming (SRP).

Synchronous reactive programming (SRP) is a well-established programming paradigm whose essential features are logical instants, broadcast events and event-based preemption. This makes it an ideal vehicle for the specification and analysis of reactive systems. Session-based concurrency is the model of concurrent computation induced by session types, a rich typing discipline designed to specify the structure of interactions.

In this work, we propose a process calculus for multiparty sessions enriched with features from SRP. In this calculus, protocol participants may broadcast messages, suspend themselves while waiting for a message, and also react to events.

Our main contribution is a session type system for this calculus, which enforces session correctness in terms of communication safety and protocol fidelity, and also ensures a time-related property, which we call input timeliness, which entails livelock-freedom. Our type system departs significantly from existing ones, specifically as it captures the notion of “logical instant” typical of SRP. This work is currently under submission.

Reversible Sessions with Flexible Choices

Reversibility has been an active trend of research for the last fifteen years. A reversible computation is a computation that has the ability to roll back to a past state. Allowing computations to reverse is a means to improve system flexibility and reliability. In the setting of concurrent process calculi, reversible computations have been first studied for CCS, then for the $\pi$-calculus, and only recently for session calculi.

Following up on our previous work on concurrent reversible sessions [29], we studied a simpler but somewhat “more realistic” calculus for concurrent reversible multiparty sessions, equipped with a flexible choice operator allowing for different sets of participants in each branch of the choice. This operator is inspired by the notion of connecting action recently introduced by Hu and Yoshida to describe protocols with optional participants. We argue that this choice operator allows for a natural description of typical communication protocols. Our calculus also supports a compact representation of the history of processes and types, which facilitates the definition of rollback. Moreover, it implements a fine-tuned strategy for backward computation. We present a session type system for the calculus and show that it enforces the expected properties of session fidelity, forward progress and backward progress. This work has been accepted for journal publication.

Multiparty sessions with Internal Delegation

We have investigated a new form of delegation for multiparty session calculi. Usually, delegation allows a session participant to appoint a participant in another session to act on her behalf. This means that delegation is inherently an inter-session mechanism, which requires session interleaving. Hence delegation falls outside the descriptive power of global types, which specify single sessions. As a consequence, properties such as deadlock-freedom or lock-freedom are difficult to ensure in the presence of delegation. Here we adopt a different view of delegation, by allowing participants to delegate tasks to each other within the same multiparty session. This way, delegation occurs within a single session (internal delegation) and may be captured by its global type. To increase flexibility in the use of delegation, our calculus uses connecting communications, which allow optional participants in the branches of choices. By these means, we are able to express conditional delegation. We present a session type system based on global types with internal delegation, and show that it ensures the usual safety properties of multiparty sessions, together with a progress property. This work is under submission.